Left Termination of the query pattern reach_in_4(g, g, g, g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

reach(X, Y, Edges, Not_Visited) :- member(.(X, .(Y, [])), Edges).
reach(X, Z, Edges, Not_Visited) :- ','(member(.(X, .(Y, [])), Edges), ','(member(Y, Not_Visited), ','(delete(Y, Not_Visited, V1), reach(Y, Z, Edges, V1)))).
member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
delete(X, .(X, Y), Y).
delete(X, .(H, T1), .(H, T2)) :- delete(X, T1, T2).

Queries:

reach(g,g,g,g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in(X, Z, Edges, Not_Visited) → U2(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U2(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U3(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U3(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U4(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U5(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
reach_in(X, Y, Edges, Not_Visited) → U1(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U1(X, Y, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → reach_out(X, Y, Edges, Not_Visited)
U5(X, Z, Edges, Not_Visited, reach_out(Y, Z, Edges, V1)) → reach_out(X, Z, Edges, Not_Visited)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4)  =  reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
U3(x1, x2, x3, x4, x5, x6)  =  U3(x2, x3, x4, x5, x6)
U4(x1, x2, x3, x4, x5, x6)  =  U4(x2, x3, x5, x6)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
U5(x1, x2, x3, x4, x5)  =  U5(x5)
U1(x1, x2, x3, x4, x5)  =  U1(x5)
reach_out(x1, x2, x3, x4)  =  reach_out

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in(X, Z, Edges, Not_Visited) → U2(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U2(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U3(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U3(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U4(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U5(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
reach_in(X, Y, Edges, Not_Visited) → U1(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U1(X, Y, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → reach_out(X, Y, Edges, Not_Visited)
U5(X, Z, Edges, Not_Visited, reach_out(Y, Z, Edges, V1)) → reach_out(X, Z, Edges, Not_Visited)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4)  =  reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
U3(x1, x2, x3, x4, x5, x6)  =  U3(x2, x3, x4, x5, x6)
U4(x1, x2, x3, x4, x5, x6)  =  U4(x2, x3, x5, x6)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
U5(x1, x2, x3, x4, x5)  =  U5(x5)
U1(x1, x2, x3, x4, x5)  =  U1(x5)
reach_out(x1, x2, x3, x4)  =  reach_out


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

REACH_IN(X, Z, Edges, Not_Visited) → U21(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
REACH_IN(X, Z, Edges, Not_Visited) → MEMBER_IN(.(X, .(Y, [])), Edges)
MEMBER_IN(X, .(H, L)) → U61(X, H, L, member_in(X, L))
MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)
U21(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U31(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U21(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → MEMBER_IN(Y, Not_Visited)
U31(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U41(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
U31(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → DELETE_IN(Y, Not_Visited, V1)
DELETE_IN(X, .(H, T1), .(H, T2)) → U71(X, H, T1, T2, delete_in(X, T1, T2))
DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)
U41(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U51(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
U41(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → REACH_IN(Y, Z, Edges, V1)
REACH_IN(X, Y, Edges, Not_Visited) → U11(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
REACH_IN(X, Y, Edges, Not_Visited) → MEMBER_IN(.(X, .(Y, [])), Edges)

The TRS R consists of the following rules:

reach_in(X, Z, Edges, Not_Visited) → U2(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U2(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U3(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U3(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U4(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U5(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
reach_in(X, Y, Edges, Not_Visited) → U1(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U1(X, Y, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → reach_out(X, Y, Edges, Not_Visited)
U5(X, Z, Edges, Not_Visited, reach_out(Y, Z, Edges, V1)) → reach_out(X, Z, Edges, Not_Visited)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4)  =  reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
U3(x1, x2, x3, x4, x5, x6)  =  U3(x2, x3, x4, x5, x6)
U4(x1, x2, x3, x4, x5, x6)  =  U4(x2, x3, x5, x6)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
U5(x1, x2, x3, x4, x5)  =  U5(x5)
U1(x1, x2, x3, x4, x5)  =  U1(x5)
reach_out(x1, x2, x3, x4)  =  reach_out
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x1, x2)
U51(x1, x2, x3, x4, x5)  =  U51(x5)
REACH_IN(x1, x2, x3, x4)  =  REACH_IN(x1, x2, x3, x4)
U41(x1, x2, x3, x4, x5, x6)  =  U41(x2, x3, x5, x6)
MEMBER_IN(x1, x2)  =  MEMBER_IN(x2)
U21(x1, x2, x3, x4, x5)  =  U21(x2, x3, x4, x5)
U11(x1, x2, x3, x4, x5)  =  U11(x5)
U71(x1, x2, x3, x4, x5)  =  U71(x2, x5)
U61(x1, x2, x3, x4)  =  U61(x4)
U31(x1, x2, x3, x4, x5, x6)  =  U31(x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

REACH_IN(X, Z, Edges, Not_Visited) → U21(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
REACH_IN(X, Z, Edges, Not_Visited) → MEMBER_IN(.(X, .(Y, [])), Edges)
MEMBER_IN(X, .(H, L)) → U61(X, H, L, member_in(X, L))
MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)
U21(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U31(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U21(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → MEMBER_IN(Y, Not_Visited)
U31(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U41(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
U31(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → DELETE_IN(Y, Not_Visited, V1)
DELETE_IN(X, .(H, T1), .(H, T2)) → U71(X, H, T1, T2, delete_in(X, T1, T2))
DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)
U41(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U51(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
U41(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → REACH_IN(Y, Z, Edges, V1)
REACH_IN(X, Y, Edges, Not_Visited) → U11(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
REACH_IN(X, Y, Edges, Not_Visited) → MEMBER_IN(.(X, .(Y, [])), Edges)

The TRS R consists of the following rules:

reach_in(X, Z, Edges, Not_Visited) → U2(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U2(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U3(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U3(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U4(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U5(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
reach_in(X, Y, Edges, Not_Visited) → U1(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U1(X, Y, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → reach_out(X, Y, Edges, Not_Visited)
U5(X, Z, Edges, Not_Visited, reach_out(Y, Z, Edges, V1)) → reach_out(X, Z, Edges, Not_Visited)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4)  =  reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
U3(x1, x2, x3, x4, x5, x6)  =  U3(x2, x3, x4, x5, x6)
U4(x1, x2, x3, x4, x5, x6)  =  U4(x2, x3, x5, x6)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
U5(x1, x2, x3, x4, x5)  =  U5(x5)
U1(x1, x2, x3, x4, x5)  =  U1(x5)
reach_out(x1, x2, x3, x4)  =  reach_out
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x1, x2)
U51(x1, x2, x3, x4, x5)  =  U51(x5)
REACH_IN(x1, x2, x3, x4)  =  REACH_IN(x1, x2, x3, x4)
U41(x1, x2, x3, x4, x5, x6)  =  U41(x2, x3, x5, x6)
MEMBER_IN(x1, x2)  =  MEMBER_IN(x2)
U21(x1, x2, x3, x4, x5)  =  U21(x2, x3, x4, x5)
U11(x1, x2, x3, x4, x5)  =  U11(x5)
U71(x1, x2, x3, x4, x5)  =  U71(x2, x5)
U61(x1, x2, x3, x4)  =  U61(x4)
U31(x1, x2, x3, x4, x5, x6)  =  U31(x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 3 SCCs with 8 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)

The TRS R consists of the following rules:

reach_in(X, Z, Edges, Not_Visited) → U2(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U2(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U3(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U3(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U4(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U5(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
reach_in(X, Y, Edges, Not_Visited) → U1(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U1(X, Y, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → reach_out(X, Y, Edges, Not_Visited)
U5(X, Z, Edges, Not_Visited, reach_out(Y, Z, Edges, V1)) → reach_out(X, Z, Edges, Not_Visited)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4)  =  reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
U3(x1, x2, x3, x4, x5, x6)  =  U3(x2, x3, x4, x5, x6)
U4(x1, x2, x3, x4, x5, x6)  =  U4(x2, x3, x5, x6)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
U5(x1, x2, x3, x4, x5)  =  U5(x5)
U1(x1, x2, x3, x4, x5)  =  U1(x5)
reach_out(x1, x2, x3, x4)  =  reach_out
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(H, T1)) → DELETE_IN(X, T1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)

The TRS R consists of the following rules:

reach_in(X, Z, Edges, Not_Visited) → U2(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U2(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U3(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U3(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U4(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U5(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
reach_in(X, Y, Edges, Not_Visited) → U1(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U1(X, Y, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → reach_out(X, Y, Edges, Not_Visited)
U5(X, Z, Edges, Not_Visited, reach_out(Y, Z, Edges, V1)) → reach_out(X, Z, Edges, Not_Visited)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4)  =  reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
U3(x1, x2, x3, x4, x5, x6)  =  U3(x2, x3, x4, x5, x6)
U4(x1, x2, x3, x4, x5, x6)  =  U4(x2, x3, x5, x6)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
U5(x1, x2, x3, x4, x5)  =  U5(x5)
U1(x1, x2, x3, x4, x5)  =  U1(x5)
reach_out(x1, x2, x3, x4)  =  reach_out
MEMBER_IN(x1, x2)  =  MEMBER_IN(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
MEMBER_IN(x1, x2)  =  MEMBER_IN(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN(.(H, L)) → MEMBER_IN(L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

REACH_IN(X, Z, Edges, Not_Visited) → U21(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U41(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → REACH_IN(Y, Z, Edges, V1)
U31(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U41(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
U21(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U31(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))

The TRS R consists of the following rules:

reach_in(X, Z, Edges, Not_Visited) → U2(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U2(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U3(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))
U3(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U4(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → U5(X, Z, Edges, Not_Visited, reach_in(Y, Z, Edges, V1))
reach_in(X, Y, Edges, Not_Visited) → U1(X, Y, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U1(X, Y, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → reach_out(X, Y, Edges, Not_Visited)
U5(X, Z, Edges, Not_Visited, reach_out(Y, Z, Edges, V1)) → reach_out(X, Z, Edges, Not_Visited)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4)  =  reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
U3(x1, x2, x3, x4, x5, x6)  =  U3(x2, x3, x4, x5, x6)
U4(x1, x2, x3, x4, x5, x6)  =  U4(x2, x3, x5, x6)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
U5(x1, x2, x3, x4, x5)  =  U5(x5)
U1(x1, x2, x3, x4, x5)  =  U1(x5)
reach_out(x1, x2, x3, x4)  =  reach_out
REACH_IN(x1, x2, x3, x4)  =  REACH_IN(x1, x2, x3, x4)
U41(x1, x2, x3, x4, x5, x6)  =  U41(x2, x3, x5, x6)
U21(x1, x2, x3, x4, x5)  =  U21(x2, x3, x4, x5)
U31(x1, x2, x3, x4, x5, x6)  =  U31(x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

REACH_IN(X, Z, Edges, Not_Visited) → U21(X, Z, Edges, Not_Visited, member_in(.(X, .(Y, [])), Edges))
U41(X, Z, Edges, Not_Visited, Y, delete_out(Y, Not_Visited, V1)) → REACH_IN(Y, Z, Edges, V1)
U31(X, Z, Edges, Not_Visited, Y, member_out(Y, Not_Visited)) → U41(X, Z, Edges, Not_Visited, Y, delete_in(Y, Not_Visited, V1))
U21(X, Z, Edges, Not_Visited, member_out(.(X, .(Y, [])), Edges)) → U31(X, Z, Edges, Not_Visited, Y, member_in(Y, Not_Visited))

The TRS R consists of the following rules:

member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
delete_in(X, .(H, T1), .(H, T2)) → U7(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U7(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))

The argument filtering Pi contains the following mapping:
member_in(x1, x2)  =  member_in(x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U6(x1, x2, x3, x4)  =  U6(x4)
member_out(x1, x2)  =  member_out(x1)
delete_in(x1, x2, x3)  =  delete_in(x1, x2)
U7(x1, x2, x3, x4, x5)  =  U7(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x3)
REACH_IN(x1, x2, x3, x4)  =  REACH_IN(x1, x2, x3, x4)
U41(x1, x2, x3, x4, x5, x6)  =  U41(x2, x3, x5, x6)
U21(x1, x2, x3, x4, x5)  =  U21(x2, x3, x4, x5)
U31(x1, x2, x3, x4, x5, x6)  =  U31(x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN(X, Z, Edges, Not_Visited) → U21(Z, Edges, Not_Visited, member_in(Edges))
U31(Z, Edges, Not_Visited, Y, member_out(Y)) → U41(Z, Edges, Y, delete_in(Y, Not_Visited))
U41(Z, Edges, Y, delete_out(V1)) → REACH_IN(Y, Z, Edges, V1)
U21(Z, Edges, Not_Visited, member_out(.(X, .(Y, [])))) → U31(Z, Edges, Not_Visited, Y, member_in(Not_Visited))

The TRS R consists of the following rules:

member_in(.(H, L)) → U6(member_in(L))
member_in(.(H, L)) → member_out(H)
delete_in(X, .(H, T1)) → U7(H, delete_in(X, T1))
delete_in(X, .(X, Y)) → delete_out(Y)
U6(member_out(X)) → member_out(X)
U7(H, delete_out(T2)) → delete_out(.(H, T2))

The set Q consists of the following terms:

member_in(x0)
delete_in(x0, x1)
U6(x0)
U7(x0, x1)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U31(Z, Edges, Not_Visited, Y, member_out(Y)) → U41(Z, Edges, Y, delete_in(Y, Not_Visited))
The remaining pairs can at least be oriented weakly.

REACH_IN(X, Z, Edges, Not_Visited) → U21(Z, Edges, Not_Visited, member_in(Edges))
U41(Z, Edges, Y, delete_out(V1)) → REACH_IN(Y, Z, Edges, V1)
U21(Z, Edges, Not_Visited, member_out(.(X, .(Y, [])))) → U31(Z, Edges, Not_Visited, Y, member_in(Not_Visited))
Used ordering: Polynomial interpretation [25]:

POL(.(x1, x2)) = 1 + x2   
POL(REACH_IN(x1, x2, x3, x4)) = 1 + x4   
POL(U21(x1, x2, x3, x4)) = 1 + x3   
POL(U31(x1, x2, x3, x4, x5)) = 1 + x3   
POL(U41(x1, x2, x3, x4)) = x4   
POL(U6(x1)) = 0   
POL(U7(x1, x2)) = 1 + x2   
POL([]) = 0   
POL(delete_in(x1, x2)) = x2   
POL(delete_out(x1)) = 1 + x1   
POL(member_in(x1)) = 0   
POL(member_out(x1)) = 0   

The following usable rules [17] were oriented:

U7(H, delete_out(T2)) → delete_out(.(H, T2))
delete_in(X, .(X, Y)) → delete_out(Y)
delete_in(X, .(H, T1)) → U7(H, delete_in(X, T1))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN(X, Z, Edges, Not_Visited) → U21(Z, Edges, Not_Visited, member_in(Edges))
U41(Z, Edges, Y, delete_out(V1)) → REACH_IN(Y, Z, Edges, V1)
U21(Z, Edges, Not_Visited, member_out(.(X, .(Y, [])))) → U31(Z, Edges, Not_Visited, Y, member_in(Not_Visited))

The TRS R consists of the following rules:

member_in(.(H, L)) → U6(member_in(L))
member_in(.(H, L)) → member_out(H)
delete_in(X, .(H, T1)) → U7(H, delete_in(X, T1))
delete_in(X, .(X, Y)) → delete_out(Y)
U6(member_out(X)) → member_out(X)
U7(H, delete_out(T2)) → delete_out(.(H, T2))

The set Q consists of the following terms:

member_in(x0)
delete_in(x0, x1)
U6(x0)
U7(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 3 less nodes.